Simplification pass #256
Simplification pass #256
Conversation
WIP Memory copyprop
* preorder iterator * add pass to inline invariant proc params * autofmt * add test for mem reasoning * print boogie code failing verification * only inline dont remove outparam for spec * single-pass variable indexing analysis to replace IntraSSA * remove ssa analysis * disable R30_out=R30_in assertion on main procedure Main will often maintain the stack by loading R30 from its caller's stack frame before returning, which makes the R30 assertion fail. Instead of disabling the assertion, in the future we should add a precondition for the stack layout before main but the interaction between spec and static analysis is no implemented yet. * fix bug in outparam inlining, still breaks dsa form * outparam inlining maintain dsa * iterate outparam inlining * convert indirectcall to call to trampoline * pprint assert comments * recognise linux __assert_fail * recognise svcomp structures * fix inlining dsa invariant * interproc frame analysis --------- Co-authored-by: l-kent <[email protected]> Co-authored-by: l-kent <[email protected]>
* Lattice sets and maps * Product domains and disjunctive completions * Fix lattice map joins on bottom * Move bounding a disjunctive completion to a seperate method * Explain disjunctive completions
* support new lifter error format * more debugging asserts * fix cilvisitor repeatbits * keep going on lift failure * escape dotgraph label
|
It would be nice to have some top-level comments (e.g. on class SimpExpr) to give an overview of how simplification works and what transforms the 'simplifier' argument can do. Should this be listed as an extra translation phase in docs/readme.md? |
constraint generation
|
I've added some docs here, mainly api docs on simplifyExpr and AbsInt and the simplification pass summary to the markdown. #318. |
ailrst
force-pushed
the
simplification-pass
branch
from
cf09f7b to
5c4df37
Compare
There was a problem hiding this comment.
Looks good.
Lots of enhancements, including interpreters, simplifiers, parameter inference etc.
Some of the docs should be updated (e.g. update interpreter.md to mention where more intrinsics are implemented) and some of the monad definitions might benefit from more docs or references so new programmers can understand the concepts.
But these can be updated after merge.
|
Merged simplification pass into main, before adding the scalafmt changes, to give a clearer history of the merge. |
Adds the flag
--simplify(which implies--parameter-form) which, after running analysis performs partial evaluation and simplification of the IR.This usually removes the flag registers and pushes the comparisons into the assume statements where they are used, folds constants through and does some canonicalisation and term simplification.
It sits on top of the interpreter #241 for partial evaluation, and includes improvements to the parameter form which I will copy into that PR #255. When #243 is merged we should use the interpreter to validate the transform using the memory state hash the csmith examples produce. Currently this is just validated against the system tests, all of which pass with the transform applied.
this implements:
The simplification/partial eval/copyprop rewrites are applied repeatedly with a fixed number of iterations.
For an example of what simplifications this produces: https://gist.github.com/ailrst/1b29e85a6ad891810dcc83801b1e2c6a